Domini funzionali e cartesiani

Un dominio è, nella pratica della semantica denotazionale, una CPO $_{⊥}$ : un ordine parziale completo dotato di elemento minimo $⊥$ . Questo articolo dà per acquisita la teoria degli ordini, poset, catene e lub, CPO e CPO $_{⊥}$ , funzioni monotone e continue, Teorema di Kleene, e si concentra su un'altra domanda: come si costruiscono i domini in modo compositivo, e perché le funzioni che vi operano risultano continue.

La motivazione è dare semantica denotazionale a un linguaggio funzionale tipato (l'esempio di riferimento è HOFL, Higher-Order Functional Language). Servono allora non un dominio, ma una famiglia intera: un dominio $D_{τ}$ per ciascun tipo $τ : : = int ∣ τ_{0} * τ_{1} ∣ τ_{0} \to τ_{1}$ in modo che ogni termine $t : τ$ denoti un valore $[[t]] ρ \in D_{τ}$ (dove $ρ$ è un ambiente type-sensitive che assegna alle variabili valori del dominio giusto). Inoltre, poiché HOFL ha la ricorsione $rec x . t$ , il significato si ottiene risolvendo un'equazione ricorsiva tramite $fix$ , e quindi ogni $D_{τ}$ deve essere una CPO $_{⊥}$ e ogni funzionale coinvolto deve essere continuo.

La strategia è compositiva: si fissa il dominio base $D_{int}$ e si forniscono dei costruttori che, dati $D_{τ_{0}}$ e $D_{τ_{1}}$ , producono $D_{τ_{0} * τ_{1}}$ e $D_{τ_{0} \to τ_{1}}$ . Il requisito cruciale è che ogni costruttore preservi la struttura di CPO $_{⊥}$ , e che le operazioni associate (proiezioni, applicazione, ricorsione…) siano continue.

Il dominio piatto degli interi

Il tipo base si interpreta nel dominio piatto $D_{int} = ℤ_{⊥}$ : gli interi più un $⊥$ che rappresenta la non terminazione. Essendo un ordine piatto è automaticamente una CPO $_{⊥}$ (ha bottom e ammette solo catene finite).

Le operazioni aritmetiche $o p \in {+, \times}$ si sollevano al dominio piatto come estensioni strette $o p_{⊥} : ℤ_{⊥} \times ℤ_{⊥} \to ℤ_{⊥}$ : il risultato $v_{1} mathbin o p_{⊥} v_{2}$ vale $v_{1} mathbin o p v_{2}$ quando entrambi gli argomenti sono interi ( $v_{1}, v_{2} \in ℤ$ ), e vale $⊥$ altrimenti (cioè non appena $v_{1} = ⊥$ oppure $v_{2} = ⊥$ ).

"Stretta" significa che $⊥$ si propaga: se un argomento diverge, diverge il risultato. Queste funzioni sono monotone e continue, automaticamente, poiché il loro dominio $ℤ_{⊥} \times ℤ_{⊥}$ ammette solo catene finite (vale il lemma "niente catene infinite $\Rightarrow$ monotona = continua").

Prodotto cartesiano di domini

Date due CPO $_{⊥}$ $D$ ed $E$ , il prodotto cartesiano $D \times E$ si ordina componente per componente: $(d_{0}, e_{0}) ⊑_{D \times E} (d_{1}, e_{1}) \Leftrightarrow d_{0} ⊑_{D} d_{1} \land e_{0} ⊑_{E} e_{1}$

Si verifica che $D \times E$ è ancora una CPO $_{⊥}$ :

è un poset: riflessività, antisimmetria e transitività si ereditano da quelle di $D$ ed $E$ ;
ha bottom $⊥_{D \times E} = (⊥_{D}, ⊥_{E})$ , perché $(⊥_{D}, ⊥_{E}) ⊑ (d, e)$ per ogni coppia;
è completo: il lub di una catena ${(d_{i}, e_{i})}$ si calcola componente per componente,

$⨆_{i \in ℕ} (d_{i}, e_{i}) = (⨆_{i \in ℕ} d_{i}, ⨆_{i \in ℕ} e_{i})$ È un maggiorante (ogni componente lo è) ed è il minimo dei maggioranti (se $(d, e)$ maggiora la catena, allora $d$ maggiora ${d_{i}}$ ed $e$ maggiora ${e_{i}}$ , da cui la disuguaglianza componente per componente).

Le proiezioni $π_{1} (d, e) = d$ e $π_{2} (d, e) = e$ sono monotone e continue. La continuità di $π_{1}$ , ad esempio, è immediata dalla definizione di lub di coppie: $π_{1} (⨆_{i} (d_{i}, e_{i})) = π_{1} (⨆_{i} d_{i}, ⨆_{i} e_{i}) = ⨆_{i} d_{i} = ⨆_{i} π_{1} (d_{i}, e_{i})$

Variante: prodotto smashed. Talvolta si usa il prodotto "schiacciato" $D \otimes E$ , che identifica in un unico bottom tutte le coppie con almeno una componente indefinita. È un buon esercizio verificare che anch'esso è una CPO $_{⊥}$ .

Switch lemma

Prima di affrontare lo spazio delle funzioni serve uno strumento tecnico, tanto semplice da enunciare quanto utile: lo switch lemma, che dice quando è lecito scambiare l'ordine di due lub annidati.

Lemma (switch). Sia $E$ una CPO e ${e_{n, m}}_{n, m \in ℕ}$ una famiglia doppiamente indicizzata, monotona in entrambi gli indici: $e_{n, m} ⊑ e_{n^{'}, m^{'}} se n \leq n^{'} \land m \leq m^{'}$ Allora ogni riga, ogni colonna e la diagonale sono catene, e i tre modi di "saturare" la matrice coincidono: $⨆_{n \in ℕ} ⨆_{m \in ℕ} e_{n, m} = ⨆_{m \in ℕ} ⨆_{n \in ℕ} e_{n, m} = ⨆_{k \in ℕ} e_{k, k}$

Idea della dimostrazione. Si prova che tutti questi insiemi hanno lo stesso insieme di maggioranti (per riga: ogni elemento di una riga sta sotto al lub di riga; per diagonale: ogni $e_{n, m}$ sta sotto a $e_{k, k}$ con $k = \max {n, m}$ , perché $n \leq k$ e $m \leq k$ ). Avendo gli stessi maggioranti, hanno lo stesso minimo dei maggioranti. $■$

Intuitivamente: per calcolare il limite di una "matrice crescente" si può procedere per righe, per colonne o lungo la diagonale, ottenendo sempre lo stesso risultato.

Spazio delle funzioni

Date due CPO $_{⊥}$ $D$ ed $E$ , il dominio funzionale $[D \to E]$ è l'insieme delle funzioni continue da $D$ a $E$ , non tutte le funzioni, solo quelle continue, ordinate punto a punto: $f ⊑_{[D \to E]} g \Leftrightarrow \forall d \in D . f (d) ⊑_{E} g (d)$

Conviene avere in mente alcuni esempi su $[ℤ_{⊥} \to ℤ_{⊥}]$ . Due funzioni totali distinte sono sempre inconfrontabili (ogni funzione totale è massimale): per avere $f ⊑ g$ con $f \neq g$ occorre che $f$ sia indefinita ( $⊥$ ) là dove $g$ è definita, e che coincidano altrove. L'ordine $⊑_{[D \to E]}$ misura quindi quanto una funzione "raffina" l'altra estendendone il dominio di definizione.

Anche $[D \to E]$ è una CPO $_{⊥}$ :

è un poset, con relazione ereditata punto a punto da $E$ ;
ha bottom $⊥_{[D \to E]} = λ d . ⊥_{E}$ , la funzione ovunque indefinita;
è completo, e questo richiede due passi.

1. Ogni catena di funzioni ${f_{n}}$ (anche non continue) ha come lub la funzione definita punto a punto $h = λ d . ⨆_{n \in ℕ} f_{n} (d) cioè h (d) = ⨆_{n} f_{n} (d)$ che è un maggiorante ed è il minimo dei maggioranti (entrambe le verifiche si fanno punto a punto). 2. Se le $f_{n}$ sono continue, allora anche $h$ lo è, ed è qui che interviene lo switch lemma. Data una catena ${d_{i}}$ in $D$ : $h (⨆_{i} d_{i}) = ⨆_{n} f_{n} (⨆_{i} d_{i}) = ⨆_{n} ⨆_{i} f_{n} (d_{i}) = ⨆_{i} ⨆_{n} f_{n} (d_{i}) = ⨆_{i} h (d_{i})$ Lo scambio centrale dei due lub è lecito perché la famiglia $e_{n, i} = f_{n} (d_{i})$ è monotona in entrambi gli indici: se $n \leq m$ e $i \leq j$ allora $f_{n} (d_{i}) ⊑ f_{n} (d_{j}) ⊑ f_{m} (d_{j})$ (per continuità/monotonia di $f_{n}$ e per $f_{n} ⊑ f_{m}$ ).

Poiché il limite di una catena di funzioni continue è continuo, esso appartiene a $[D \to E]$ , che risulta dunque chiuso e completo. Ricordiamo infine che la composizione di funzioni continue è continua, cioè se $f \in [D \to E]$ e $g \in [E \to F]$ allora $g \circ f \in [D \to F]$ .

Domini sollevati e somma disgiunta

Per completare la cassetta degli attrezzi servono altri due costruttori.

Il sollevamento (lifting) di una CPO $D$ è $D_{⊥} = {⊥} ⊎ D$ . Attenzione: non è l'ordine piatto. Il lifting aggiunge un nuovo bottom strettamente sotto a una copia fedele $⌊ d ⌋$ di $D$ , conservandone l'ordine interno: $⊥_{D_{⊥}} ⊑ x \forall x; ⌊ d_{1} ⌋ ⊑_{D_{⊥}} ⌊ d_{2} ⌋ \Leftrightarrow d_{1} ⊑_{D} d_{2}$ È una CPO $_{⊥}$ , con $⨆_{i} ⌊ d_{i} ⌋ = ⌊ ⨆_{i} d_{i} ⌋$ . L'operatore di lifting ${(\cdot)}^{*} : [D \to E] \to [D_{⊥} \to E]$ trasforma $f$ in $f^{*}$ con $f^{*} (⊥) = ⊥_{E}$ e $f^{*} (⌊ d ⌋) = f (d)$ : è ben definito, monotono e continuo. Su di esso si basa la comoda notazione di de-lifting $let x \Leftarrow t . e$ , che estrae il valore da $t$ (se definito) e lo assegna a $x$ in $e$ , propagando altrimenti $⊥_{E}$ .

La somma disgiunta $D + E = (D ⊎ E, ⊑)$ affianca i due domini tenendoli separati (tramite iniezioni continue $ι_{D}, ι_{E}$ ); serve a interpretare i tipi unione. La costruzione dell'ordine, del bottom e delle iniezioni è un utile esercizio.

Teoremi di continuità

Verificare la continuità "a mano" di ogni funzione semantica sarebbe poco pratico. I teoremi di continuità permettono di ridurre il problema a controlli più semplici, e forniscono un compendio di operatori già noti essere continui.

Continuità sul codominio prodotto

Teorema. Sia $f : D \to E_{1} \times E_{2}$ e poniamo $g_{i} = π_{i} \circ f$ . Allora $f$ è continua se e solo se $g_{1}$ e $g_{2}$ lo sono.

La direzione $(\Rightarrow)$ segue dal fatto che le proiezioni sono continue e la composizione di funzioni continue è continua. La direzione $(\Leftarrow)$ si calcola componente per componente, usando che $f (d) = (g_{1} (d), g_{2} (d))$ e che il lub nelle coppie è componente per componente. In pratica: una funzione a valori in un prodotto è continua esattamente quando lo sono le sue componenti.

Continuità separata sugli argomenti

Teorema. Sia $f : D \times E \to F$ . Definite le applicazioni parziali $f_{d} = λ e . f (d, e) : E \to F f_{e} = λ d . f (d, e) : D \to F$ allora $f$ è continua se e solo se $f_{d}$ è continua per ogni $d \in D$ e $f_{e}$ è continua per ogni $e \in E$ .

Questo è uno dei risultati più usati: per stabilire la continuità di una funzione a due argomenti basta controllarla un argomento alla volta. La direzione delicata è $(\Leftarrow)$ : data una catena ${(d_{k}, e_{k})}$ in $D \times E$ , si separa il lub di coppie e si applica la continuità prima su un argomento e poi sull'altro, usando infine lo switch lemma per ricomporre il doppio lub $f (⨆_{k} (d_{k}, e_{k})) = ⨆_{j} ⨆_{i} f (d_{i}, e_{j}) = ⨆_{k} f (d_{k}, e_{k})$ applicabile perché $f (d_{i}, e_{j})$ è monotona in $i$ e in $j$ (le applicazioni parziali sono monotone).

Attenzione. Continuità (e perfino monotonia) separata va verificata con cura: una funzione può essere ben definita "come grafo" ma non monotona se "guarda" se un argomento è $⊥$ . Ad esempio $g (x, y) = x \cdot y$ se $x, y \neq ⊥$ e $g (⊥, y) = 0$ non è nemmeno monotona, perché $g (⊥, ⊥) = 0 not ⊑$ valori prodotti quando gli argomenti si raffinano.

Operatori fondamentali

I teoremi precedenti permettono di dimostrare che i costituenti della semantica denotazionale sono continui:

Applicazione $apply : [D \to E] \times D \to E$ , con $apply (f, d) = f (d)$ , è continua (la si verifica separatamente nei due argomenti: fissato $f$ è continua perché $f$ lo è; fissato $d$ è continua per la definizione di lub punto a punto nel dominio funzionale). Dunque $apply \in [[D \to E] \times D \to E]$ .
Punto fisso $fix : [D \to D] \to D$ , con $fix = λ f . ⨆_{n} f^{n} (⊥_{D})$ , è esso stesso continuo. La dimostrazione mostra per induzione su $n$ che ogni $λ f . f^{n} (⊥_{D})$ è continua (caso base: funzione costante $λ f . ⊥_{D}$ ; passo induttivo: usa lo switch lemma), e poi conclude che $fix$ è continua perché lub di funzioni continue. Questo è esattamente ciò che rende ben definita e compositiva la denotazione di $rec x . t$ .
Currying $curry : [D \times E \to F] \to [D \to [E \to F]]$ e il suo inverso $uncurry$ preservano la continuità e sono mutuamente inversi: stabiliscono l'isomorfismo $[D \times E \to F] ≅ [D \to [E \to F]]$ , la versione "su domini" della corrispondenza tra funzioni a due argomenti e funzioni che restituiscono funzioni.

In definitiva, i costruttori (prodotto, spazio funzionale, lifting, somma) sono chiusi rispetto alla struttura di CPO $_{⊥}$ , e gli operatori fondamentali sono continui: abbiamo così un linguaggio completo per costruire, in modo compositivo, i domini e le funzioni semantiche di un linguaggio funzionale di ordine superiore.